es:ES, P, Q:(E), R:(EE), f1:({e:E| P(e)} {e:E| Q(e)} ), f2:({e:E| Q(e)} E).
(f1 is R-pre-preserving on P & f2 is R-pre-preserving on Q)
 f2 o f1 is R-pre-preserving on P 

latex

Definitions	f is R-pre-preserving on P, ES, t  T, Type, , x:A. B(x), E, x:AB(x), f(a), {x:A| B(x)} , f is Q-R-pre-preserving on P, S  T, suptype(S; T), x:A  B(x), P & Q, P  Q
Lemmas	Q-R-pre-preserving-compose, Q-R-pre-preserving wf, es-E wf, event system wf